<html>
<head><meta charset="utf-8"><title>Proofs of soundness · t-compiler/wg-mir-opt · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/index.html">t-compiler/wg-mir-opt</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html">Proofs of soundness</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="201697954"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201697954" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201697954">(Jun 23 2020 at 08:10)</a>:</h4>
<p>So. My vision for our fancy MIR-future where we do all sorts of cool stuff with mir opts includes the idea of proving the soundness of the transformations we make while optimizing MIR.</p>
<p>This is of course a long term project more than a "right now" thing. Specially because it would need a precise understanding of MIR semantics, which haven't yet been fully defined if I understood correctly.</p>
<p>BUT. I want to help push this forward at some point. I don't know if I can do a good job of it, I don't know if there's a tool for this, and I only sort of understand one of the opts (the const-prop one). Still, I think it would be really good to have.</p>
<p>So:<br>
Have there been discussions on this topic? Also, is there a group in the community that has experience proving these kinds of things?</p>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span> you've probably thought about this at some point, right? :3<br>
Anywho, I ping you because I'd figure you'd want to chip in here ^^</p>



<a name="201703821"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201703821" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201703821">(Jun 23 2020 at 09:16)</a>:</h4>
<p>The Stacked Borrows paper (<a href="https://plv.mpi-sws.org/rustbelt/stacked-borrows/">https://plv.mpi-sws.org/rustbelt/stacked-borrows/</a>) includes proofs for some optimizations justified by the aliasing rules -- though, as far as I can tell, only for some specific pairs of programs which illustrate the desired optimization (rather than giving an optimization algorithm, and then proving it correct for all programs). A noteworthy alternative/complement to traditional "pen and paper" (or Coq) formalization of algorithms is  <em>translation validation</em>,  which addresses the problem of gaps between the formalization of the optimization and its production implementation. The Alive project (<a href="https://blog.regehr.org/archives/1722">https://blog.regehr.org/archives/1722</a>) has been doing this very successfully with LLVM optimizations, a similar approach may be effective for MIR optimizations once we have precise semantics for it.</p>



<a name="201723012"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201723012" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201723012">(Jun 23 2020 at 13:13)</a>:</h4>
<p>(Though I do wonder if/how translation from IR to SMT formulas, as done in Alive, can be reconciled with MIR being polymorphic. Last I heard, even generalizing over integer bit widths was an area of active research. Perhaps the simple approach of "try some concrete instances and hope that will catch most bugs"  will be good enough for a start?)</p>



<a name="201751643"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201751643" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201751643">(Jun 23 2020 at 16:48)</a>:</h4>
<p><span class="user-mention" data-user-id="212698">@Félix Fischer</span> the "formal-methods" stream might be a better fit for this topic, actually :)</p>



<a name="201751768"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201751768" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201751768">(Jun 23 2020 at 16:49)</a>:</h4>
<p>I have many thoughts, indeed.^^ but realistically, rustc isn't going to get CompCert-style Coq proofs. Those are too much work, there are too few people who can do them, and there is now they they could keep up with Rust's development pace.</p>



<a name="201751798"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201751798" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201751798">(Jun 23 2020 at 16:49)</a>:</h4>
<p>So I think our best bet is something like Alive2, as mentioned by <span class="user-mention" data-user-id="124289">@Hanna Kruppe</span></p>



<a name="201751941"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201751941" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201751941">(Jun 23 2020 at 16:50)</a>:</h4>
<p>(the stacked borrows proofs show that some reorderings are in principle possible in an idealized Rust. this is a crucial first step, but there's a significant gap between that and verifying what our MIR optimizations are doing.)</p>



<a name="201752036"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201752036" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201752036">(Jun 23 2020 at 16:51)</a>:</h4>
<p>(also, aliasing-based optimizations are amongst the hardest to verify. I think we should start with easier ones. :D )</p>



<a name="201752100"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201752100" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201752100">(Jun 23 2020 at 16:51)</a>:</h4>
<p>coming back to Alive2, I would happily be involved with figuring out MIR semantics more precisely, but I have no idea how Alive2 does its actual checking</p>



<a name="201752170"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201752170" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201752170">(Jun 23 2020 at 16:52)</a>:</h4>
<p>my background is in doing complex proofs by hand in coq, I know little about automated theorem proving</p>



<a name="201921665"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201921665" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201921665">(Jun 25 2020 at 00:51)</a>:</h4>
<p>Ohh, I see!</p>



<a name="201921714"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201921714" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201921714">(Jun 25 2020 at 00:52)</a>:</h4>
<p>Btw <span class="user-mention" data-user-id="124289">@Hanna Kruppe</span> those are great links, thank you &lt;3</p>



<a name="201921730"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201921730" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201921730">(Jun 25 2020 at 00:52)</a>:</h4>
<p>So... I was thinking more of doing proofs by hand</p>



<a name="201921731"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201921731" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201921731">(Jun 25 2020 at 00:52)</a>:</h4>
<p>Like</p>



<a name="201921773"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201921773" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201921773">(Jun 25 2020 at 00:53)</a>:</h4>
<p>After we exhaust one branch of optimization (like const prop for example, in which I'm planning to put some serious effort after I get some bureaucracy done with uni, hopefully during the following weeks)</p>



<a name="201921776"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201921776" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201921776">(Jun 25 2020 at 00:53)</a>:</h4>
<p>We freeze the code, or the algorithm at least</p>



<a name="201921808"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201921808" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201921808">(Jun 25 2020 at 00:54)</a>:</h4>
<p>And we try to prove that some invariants are being held through each step of the optimization pass</p>



<a name="201921847"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201921847" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201921847">(Jun 25 2020 at 00:54)</a>:</h4>
<p>I think that just that could be big</p>



<a name="201921864"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201921864" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201921864">(Jun 25 2020 at 00:54)</a>:</h4>
<p>It would at least make us question our code's soundness and try to prove that the edge cases hold it</p>



<a name="201921975"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201921975" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201921975">(Jun 25 2020 at 00:57)</a>:</h4>
<p>I think that's most of what we need. With the algorithm being frozen, and the proof being out in the open, even if it's not actually machine-verified, it could be checked by the eyes of everyone that wants to help.</p>



<a name="201922047"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201922047" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201922047">(Jun 25 2020 at 00:58)</a>:</h4>
<p><span class="user-mention silent" data-user-id="120791">RalfJ</span> <a href="#narrow/stream/189540-t-compiler.2Fwg-mir-opt/topic/Proofs.20of.20soundness/near/201751643">said</a>:</p>
<blockquote>
<p><span class="user-mention silent" data-user-id="212698">Félix Fischer</span> the "formal-methods" stream might be a better fit for this topic, actually :)</p>
</blockquote>
<p>Haha that's fair. Is it possible to move it there?</p>



<a name="201947862"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201947862" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201947862">(Jun 25 2020 at 09:25)</a>:</h4>
<p><span class="user-mention silent" data-user-id="212698">Félix Fischer</span> <a href="#narrow/stream/189540-t-compiler.2Fwg-mir-opt/topic/Proofs.20of.20soundness/near/201921776">said</a>:</p>
<blockquote>
<p>We freeze the code, or the algorithm at least</p>
</blockquote>
<p>I strongly doubt such a freeze will ever happen...</p>



<a name="201948082"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201948082" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201948082">(Jun 25 2020 at 09:28)</a>:</h4>
<p>Right, for const prop in particular this would mean freezing both the definition of MIR (well, the subset that const prop operates on) and miri (again, at least the parts relevant to const prop). This seems very invasive and undesirable.</p>



<a name="201949666"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/201949666" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#201949666">(Jun 25 2020 at 09:49)</a>:</h4>
<p>I also have serious doubts about the value of (mechanized or pen-and-paper) proofs for this particular part. The "core" of constant evaluation is conceptually trivial once operational semantics for MIR are fixed (OTOH, picking reasonable semantics is quite challenging). This is not to say there aren't any bugs in it -- but many are either</p>
<ol>
<li>integration issues (e.g., <a href="https://github.com/rust-lang/rust/issues/67019">#67019</a> was due to not accounting for layout optimizations properly) where focusing solely on the pass itself won't help</li>
<li>Plainly incorrect transformations (e.g., <a href="https://github.com/rust-lang/rust/issues/73609">#73609</a>) that can be found just as well by simpler means than attempting proofs</li>
</ol>
<p>In my personal view, the kind of approach you described is more valuable when there's subtle invariants <em>internal</em> to a reasonably small module (e.g., a very clever data structure), because then you can actually confidently state and validate a useful invariant, rather than either verifying trivial things ("miri indeed performs an addition when there's an <code>Add</code> operation in the MIR") or having to content with many integration points.</p>



<a name="202002415"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202002415" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202002415">(Jun 25 2020 at 17:54)</a>:</h4>
<p>Ohh, I see. Both of you two expose very fair points.</p>
<p>Re: freeze<br>
I guess I didn't see that we'd have to freeze MIR and maybe miri for that (although now that I've worked on const-prop, I'm not sure what is and what isn't miri anymore. I was sure I hadn't ever touched it until someone said that it was used for const prop, so I guess all of what I did touch was actually miri? Anywho). And yeah, that sure seems invasive. Specially freezing miri. Freezing MIR seems like it could be a thing tho? Like after semantics are well defined and all of that. In the long term, there might be a day when MIR is frozen right?</p>



<a name="202002635"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202002635" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202002635">(Jun 25 2020 at 17:55)</a>:</h4>
<p>Re: proofs.<br>
I think I more or less agree with you, Hanna. That makes sense :)</p>



<a name="202002819"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202002819" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202002819">(Jun 25 2020 at 17:56)</a>:</h4>
<p>I see no reason to expect either the "surface" Rust language or rustc implementation details (e.g., internal architecture, data structures) to ever be frozen, and changes to either of those lead to MIR changes, even if they are backwards compatible changes.</p>



<a name="202004035"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202004035" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202004035">(Jun 25 2020 at 18:06)</a>:</h4>
<p>Ahh, you mean the produced MIR code</p>



<a name="202004063"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202004063" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202004063">(Jun 25 2020 at 18:07)</a>:</h4>
<p>I was thinking more on the definition and semantics of MIR itself <span aria-label="laughing" class="emoji emoji-1f606" role="img" title="laughing">:laughing:</span></p>



<a name="202004081"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202004081" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202004081">(Jun 25 2020 at 18:07)</a>:</h4>
<p>Okay, now I think I really get what you mean</p>



<a name="202004103"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202004103" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202004103">(Jun 25 2020 at 18:07)</a>:</h4>
<p>No, I mean the definition and semantics of MIR itself.</p>



<a name="202004200"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202004200" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202004200">(Jun 25 2020 at 18:08)</a>:</h4>
<p>Really? Wait, how would that cha- ohh. Okay, yeah, the compiler IS sort of the definition and semantics of MIR</p>



<a name="202004232"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202004232" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202004232">(Jun 25 2020 at 18:08)</a>:</h4>
<p>So if you change the compiler, you change MIR</p>



<a name="202004248"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202004248" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202004248">(Jun 25 2020 at 18:08)</a>:</h4>
<p>For example, the specific way NLL is done right now influences the definition of MIR statements and places, and future changes (like Polonius) will probably fit better with different representations.</p>



<a name="202004374"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202004374" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Hanna Kruppe <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202004374">(Jun 25 2020 at 18:09)</a>:</h4>
<p>(Or the other way around: changes to MIR are being proposed and running into challenges related to borrow checking; if borrow checking changes then different designs become more attractive.)</p>



<a name="202004438"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202004438" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202004438">(Jun 25 2020 at 18:09)</a>:</h4>
<p>(Right! :D)</p>



<a name="202004503"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202004503" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202004503">(Jun 25 2020 at 18:10)</a>:</h4>
<p>That makes sense</p>



<a name="202004543"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202004543" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202004543">(Jun 25 2020 at 18:10)</a>:</h4>
<p>Thank you for the explanation, Hanna ^^</p>



<a name="202178850"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202178850" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Xavier Denis <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202178850">(Jun 27 2020 at 10:20)</a>:</h4>
<p>I feel like it's much more valuable to prove the optimizations correct on a idealised version of Rust than to attempt to prove the actual implementation. At least then the gap narrows to 'does the implementation behave like the idealised version'?</p>



<a name="202205020"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202205020" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202205020">(Jun 27 2020 at 21:06)</a>:</h4>
<p>That's a good point</p>



<a name="202909186"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202909186" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202909186">(Jul 05 2020 at 07:11)</a>:</h4>
<p>yeah, that's why this is what we did with Stacked Borrows</p>



<a name="202909190"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202909190" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202909190">(Jul 05 2020 at 07:11)</a>:</h4>
<p>it's about validation that the optimizations are eight <em>in principle</em>, not that they are implemented correctly</p>



<a name="202909192"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202909192" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202909192">(Jul 05 2020 at 07:11)</a>:</h4>
<p>experience with LLVM shows that this is non-trivial in many cases</p>



<a name="202909230"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202909230" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202909230">(Jul 05 2020 at 07:12)</a>:</h4>
<p>const-prop is just very simple, conceptually, which makes it less interesting to look at here</p>



<a name="202956923"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/189540-t-compiler/wg-mir-opt/topic/Proofs%20of%20soundness/near/202956923" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Félix Fischer <a href="https://rust-lang.github.io/zulip_archive/stream/189540-t-compiler/wg-mir-opt/topic/Proofs.20of.20soundness.html#202956923">(Jul 06 2020 at 06:30)</a>:</h4>
<p>Haha, no wonder I like const-prop so much <span aria-label="big smile" class="emoji emoji-1f604" role="img" title="big smile">:big_smile:</span> it felt really approachable</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>